k:FinProbSpace, n:, i:{0..n}, X:(Outcome). X@i  RandomVariable(k;n) 

latex

Definitions	t  T, , x:A. B(x), ||as||, P & Q, i  j < k, a < b, P  Q, False, A, A  B, , {x:A| B(x)} , {i..j}, #$n, Void, x:AB(x), l[i], x. t(x), a  j < b. E(j), s = t, type List, , Type, f(a), x.A(x), X@i, RandomVariable(p;n), Outcome, FinProbSpace
Lemmas	nat wf, qsum wf, select wf, int seg wf, int inc rationals, length wf1, rationals wf